OIGJ is a Java language extension
    that supports both ownership and immutability,
    while enhancing
    the expressiveness of each individual concept.
By using Java's generic types, OIGJ simplifies previous type mechanisms,
    such as existential owners, scoped regions, and owner-polymorphic methods.
OIGJ is easy to understand and implement, using only 14 (flow-insensitive)
    typing rules beyond those of Java.
We have formalized a core calculus called FOIGJ and proved it sound.
Our implementation is backward-compatible with Java, and it scales to
realistic programs.
OIGJ can type-check Sun's \code{java.util} collections
    (without the \code{clone} method),
    using a small number of annotations.
Finally, various design patterns, such as the factory and visitor patterns, can be expressed in OIGJ,
    making it ready for practical use.
An implementation is publicly available at {\footnotesize \url{http://types.cs.washington.edu/checker-framework/}}.

Future work includes
    inferring ownership and immutability, % annotations,
    conducting a bigger case study with client and library code,
    and extending OIGJ with concepts such as
    \emph{owner-as-modifier}~\cite{ZibinEtAlOsMTR2010},
    \emph{uniqueness}, and
    \emph{external-uniqueness}~\cite{ClarkeW2003:ECOOP}.




%OIGJ ensures that the object cannot be stored on the heap,
%    which will violate the owner-as-dominator property.
%This is done in the last part of the rule by changing all the owner parameters to wildcards.
%\begin{algorithmic}
%\STATE \code{class Rect<\underline{O extends World},\underline{I extends ReadOnly}> \lb}
%\STATE \code{~~Point<\underline{This},I> p;}
%\STATE \code{~~boolean isEqualTo(Rect<?,ReadOnly> r) \lb}
%\STATE \code{~~~~return this.p.x==\underline{r.p}.x \&\& this.p.y==\underline{r.p}.y; \rb}
%\STATE \code{\rb}
%\end{algorithmic}
%
%Previous work on owner-as-dominator often use the example of a rectangle that owns its two points.
%%    and therefore the rectangle can maintain the invariant that one point is always to the left of the other.
%Field \code{p} is an example of such a \this-owned point.
%Consider method \code{isEqualTo}, and compare the two field accesses: \code{this.p} and \code{r.p}.
%The second access leaks the privately owned point, and therefore
%    was considered illegal by previous work,
%    thus leading to inefficient solutions that copy the private point.
%OIGJ takes a different approach:
%    the access \code{r.p} is allowed, but the point is leaked as readonly with a wildcard owner parameter,
%    i.e.,~\code{Point<\underline{?},ReadOnly>},
%    thus preventing anyone from mutating or storing the point on the heap.
%
%
%OIGJ supports both owner-as-dominator and owner-as-modifier,
%    enabling a programmer to choose the most appropriate tool for the problem. %between strict encapsulation or free sharing of readonly references.
%
%OIGJ subsumes Universes as follows:
%    \code{rep Foo} corresponds to OIGJ's \code{Foo<Modifier,Mutable>},
%    \code{peer Foo} corresponds to \code{Foo<O,Mutable>}, and
%    \code{any Foo} corresponds to \code{Foo<World,ReadOnly>}.

% LocalWords:  FOIGJ util
